A:Type, P:(AProp).
(s:A. Dec(k:. P(s,k)))
 (s:A, k:. Dec(P(s,k)))
 (s:A. Dec(v:. P(s,v) & (n:. n<v  P(s,n)))) 

latex

Definitions	t  T, x:A. B(x), P  Q, i  j < k, {x:A| B(x) }, x:AB(x), f(a), a<b, x:AB(x), False, n-m, Type, Prop, A & B, Void, , left+right, P  Q, Dec(P), x.A(x), x. t(x), {T}, ij, -n, n+m, x(s1,s2), A, #$n, {i..j}, x:A. B(x), s ~ t, AB, P & Q,
Lemmas	ge wf, nat properties, decidable wf, decidable ex int seg, decidable not, int seg wf, nat wf, not wf, le wf